the_w:World, e:E. first(e)  (t':. t'<time(e)  isnull(a(loc(e);t'))) 

latex

Definitions	x:A. B(x), b, first(e), t  T, Y, if b t else f fi, i=j, time(e), true, loc(e), 2of(t), 1of(t), P  Q, ij, AB, A, False, P  Q, True, P & Q, P  Q, Prop, , false, SQType(T), {T}, , Unit, Dec(P), P  Q, E,
Lemmas	nat wf, Id wf, world wf, nat properties, ge wf, true wf, assert wf, w-isnull wf, w-a wf, eq int wf, bool wf, iff transitivity, eqtt to assert, assert of eq int, btrue wf, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, le wf, w-first-aux, decidable lt, false wf, w-E wf